Business process models are known. A business process model is a model defining order dependencies of constituent activities of a business process. With the increased use of business process models in simulation, code generation and direct execution, it becomes more and more important that the processes are free of control- and data-flow errors. Various studies (see [1] for a survey) have shown that such errors frequently occur in processes.
It can be realized that some of these errors can be characterized in terms of relationships between control-flow edges or tasks of the process. For example, a process is free of deadlock if any two incoming edges of an AND-join are always marked concurrently. We can say that such a pair of edges is always concurrent. A process is free of lack of synchronization if any two incoming edges of an XOR-join are mutually exclusive, i.e., they never get marked concurrently. A data-flow hazard may arise if two conflicting operations on the same data object are executed concurrently. That can happen only if the tasks containing the data operations are sometimes concurrent, i.e., not mutually exclusive. Similar relationships have also been proposed for a behavioral comparison of processes [2, 3].
Such control-flow relations can be computed by enumerating all reachable control-flow states of the process by explicitly executing its workflow graph, i.e., its control-flow representation. However, there can be exponentially many such states, resulting in a worst-case exponential time algorithm.
Some existing techniques can decide soundness of a workflow graph without IOR gateways, or equivalently a Free Choice Petri net, in polynomial time: a technique based on the rank theorem [4] in cubic time and techniques based on a complete reduction calculus [5] in more than cubic time. However, diagnostic information is not provided by the former technique and was not yet worked out for the latter.
Techniques based on state space exploration return an error trace, i.e., an execution that exhibits the control-flow error, but they have exponential worst-case time complexity. It has been shown [6] for industrial processes without IOR gateways that the latter problem can be effectively addressed in practice using various reduction techniques. Various additional structural reduction techniques exist in the literature, e.g., [7, 8].
Wynn et al. [9] provide a study of verifying processes with IOR gateways. They apply state space exploration and use a different IOR-join semantics.
To the best of their knowledge, the present inventors are not aware of approaches that provide diagnostic information to deal with the over-approximation due to data abstraction in workflow graphs. Existing approaches to check other notions of soundness such as relaxed soundness [10] or weak soundness [11] have exponential complexity.